Nuprl Definition : w-first 0,22

first(e)
== if time(e)=0 true ; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>) else false fi
(recursive) 
latex



clarification:

w-first(w; e)
== if w-time(w; e)=0 true
== i; w-isnull(w; w-a(w; w-loc(w; e); (w-time(w; e)-1))) w-first(w; <w-loc(w; e),w-time(w; e)-1>)
== else false fi
(recursive) 
latex


DefinitionsY, x.A(x), i=j, true, if b t else f fi, isnull(a), a(i;t), f(a), <a,b>, loc(e), n-m, time(e), #$n, false
FDL editor aliasesw-first

origin